if(if(x, y, z), u, v) → if(x, if(y, u, v), if(z, u, v))
↳ QTRS
↳ DependencyPairsProof
if(if(x, y, z), u, v) → if(x, if(y, u, v), if(z, u, v))
IF(if(x, y, z), u, v) → IF(x, if(y, u, v), if(z, u, v))
IF(if(x, y, z), u, v) → IF(y, u, v)
IF(if(x, y, z), u, v) → IF(z, u, v)
if(if(x, y, z), u, v) → if(x, if(y, u, v), if(z, u, v))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
IF(if(x, y, z), u, v) → IF(x, if(y, u, v), if(z, u, v))
IF(if(x, y, z), u, v) → IF(y, u, v)
IF(if(x, y, z), u, v) → IF(z, u, v)
if(if(x, y, z), u, v) → if(x, if(y, u, v), if(z, u, v))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(if(x, y, z), u, v) → IF(x, if(y, u, v), if(z, u, v))
IF(if(x, y, z), u, v) → IF(y, u, v)
IF(if(x, y, z), u, v) → IF(z, u, v)
The value of delta used in the strict ordering is 1/8.
POL(if(x1, x2, x3)) = 1/4 + (4)x_1 + x_2 + (4)x_3
POL(IF(x1, x2, x3)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
if(if(x, y, z), u, v) → if(x, if(y, u, v), if(z, u, v))